Struct isotope::prelude::Id [−][src]
pub struct Id { /* fields omitted */ }
Expand description
The identity type, representing proofs that two terms are equal
Implementations
Create a new, unchecked instance of an identity type with a given annotation
Compute the most basic universe for an identity type
Create a new, unchecked instance of the reflexivity axiom, inferring the most basic possible annotation
Compute the code of an identity type with a given type annotation
Compute the filter of a reflexivity instance with a given type annotation
Compute the flags of a reflexivity instance with a given type annotation
Compute whether a dependent function type locally type-checks given an annotation
Compute whether a dependent function type locally type-checks given a universe
If both sides of this equality are types, get them as a universe.
Return None
if neither side is a universe, or if both sides are different universes (implying this instance is invalid!)
Trait Implementations
Cons this term within a given context. Return None
if already consed.
Convert this term to it’s own consed type
Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class
Get whether a term depends on a variable base <= variable <= ix
Read more
Get the variable filter of this term
type Substituted = Id
type Substituted = Id
The type this substitutes to
Substitute this value recursively
Convert this object’s consed form to it’s substituted form
Shift this term’s variables with index >= base
in a given context
Shift this term’s variables with index >= base
in a given context
Locally typecheck a term: note this is context-independent, without caching
Globally typecheck a term, i.e. typecheck all subterms, without caching
Typecheck this term’s annotation, without caching
Load this term’s current flags
Set this term’s flags. May cause errors if done incorrectly!
Locally typecheck a term: note this is context-independent.
Globally typecheck a term, i.e. typecheck all subterms and their variables
Variable typecheck a term, i.e. typecheck all subterms and their variables.
Typecheck this term’s annotation
Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables
Typecheck a term in a given context
Typecheck this term along with it’s variables
Whether this term might be type-checked
type ValueConsed = Id
type ValueConsed = Id
The type of value this is consed to
type ValueSubstituted = Id
type ValueSubstituted = Id
The type of value this is substituted to
Convert this term to a Term
, without any consing
Get the type annotation of this term
Get whether this term is a type
Get whether this term is a universe
Get whether this term is a function
Get whether this term is a dependent function type
Coerce this term to another type, with type-checking
fn annotate_unchecked(
&self,
_annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Id>, Error>
[src]
fn annotate_unchecked(
&self,
_annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Id>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in a given context
Get the hash-code of this term if it was untyped Read more
Compare this term to another within a given context
Get the index of this term in a program graph. Return None
if this term is unindexed
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in general
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Cast this type into another in a given typing context
Substitute this term’s variables recursively given a context
Substitute this term’s variables given a context
Shift this term’s variables with index >= base
up by n
in a given context
Shift this term’s variables with index >= base
up by n
in a given context
Compare this term to a term ID, within a given context
Cons this term within a given context. Return None
if already consed.
Convert this term to a TermId
within a given context
Get the type of this term, if any
Get the type of this term, if any
Apply this value, as a function, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Apply this value, as a dependent function type, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Convert this term to a TermId
, without any consing
Clone this term to a TermId
, without any consing
Clone this term to a TermId
within a given context
Clone this term to a Term
without any consing
Shallow cons a term directly into a context
Shallow cons a term directly into a context, cloning if necessary
Convert this term to a normal form
Convert this term a normal form
Convert this term to a normal form, or reduce it up to n
steps
Convert this term a normal form, or reduce it up to n
steps
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to a normal form, or reduce it up to n
steps
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]Convert this term a normal form, or reduce it up to n
steps
Auto Trait Implementations
Blanket Implementations
Mutably borrows from an owned value. Read more
Borrow an optional value of type T
Compare self to key
and return true
if they are equal.